#include "basic_set_operations.hh"

bdd compute_predecessors(bdd a, const Model& m)
{
  bdd a_ = m.reverse_state(a);

  bdd predecessor_relation = m.successor_relation & a_;

  bdd predecessor = bdd_exist(predecessor_relation,
			      m.reverse_state(m.get_state_high()));

  return predecessor;
}

bdd compute_successors(bdd a, const Model& m)
{
  bdd successor_relation = m.successor_relation & a;

  bdd successors = bdd_exist(successor_relation,
			     m.get_state_high());

  return m.unreverse_state(successors);
}

bdd compute_validating_states(bdd var, const Model& m)
{
  bdd validating_states = m.label_relation & var;

  return bdd_exist(validating_states, m.get_problem_variables());
}

bdd compute_not(bdd a, const Model& m)
{
  bdd W = m.label_relation;

  W = bdd_exist(W, m.get_problem_variables());

  return W - a;
}
